/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.ast;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.Set;

import alloy.semantic.LocalScope;
import alloy.transform.LeafIdMap;
import alloy.type.RelationType;
import alloy.type.SigType;
import alloy.type.UnionType;
import alloy.util.CreationInfo;
import alloy.util.Dbg;

/** AST node representing a Signature.  Signature implements Leaf
    because it holds a pointer to the LeafId of the set of atoms
    associated with the signature (except for uninstantiated
    polymorphic signatures). */

public class Signature extends TreeNode implements Paragraph, Leaf {

    /**
     * index of name in child list
     */
    private static final int NAME_INDEX = 0;

    /**
     * index of extended signature names in child list
     * NOTE: should always have at most one extended signature now
     */
    private static final int EXTENDS_INDEX = 1;

    /** index of signatures this is a subset of in child list **/
    private static final int SUBSETS_INDEX = 2;

    /**
     * index of decls in child list
     */
    private static final int DECLS_INDEX = 3;

    /**
     * index of fact in child list
     */
    private static final int FACT_INDEX = 4;

    /**
     * true if this is a product sig
     */
    private boolean _isProduct;

    /**
     * true if this is an abstract sig
     */
    private boolean _isAbstract;

    /** multiplicity of this (one, lone, some, set, or no multiplicity) **/
    private Multiplicity _mult;

    /**
     * the localscope associated with the Decls of this
     */
    private LocalScope _localScope = new LocalScope();

    /** mapping from field names to unique ids */
    private LeafIdMap _leafIdMap;

    public Set _allFieldNames;

    /**
     * the Signatures which extend this
     */
    private Set _extendedBy = new LinkedHashSet();

    /**
     * the SigType of this
     */
    private SigType _sigType;

    /**
     * the UnionType of this
     **/
    private UnionType _unionType;

    /** the id of this */
    private LeafId _id;

    /** For debugging: a record of where in the program this leaf was created */
    private CreationInfo _creationInfo = new CreationInfo();
    /** For debugging: return info on where in the program this leaf was created */
    public CreationInfo getCreationInfo() { return _creationInfo; }
  
    /** if this is a wrapper sig for skolemizing a function,
        the signature wrapped by this.  See {@link alloy.transform.FunctionSkolemizer}.
    */
    public Signature wrappedSig;

    public Signature(
        Location location_,
        QualifiedName name_,
        SigExprs extends_,
	SigExprs subsets_,
        Decls decls_,
        Fact fact_,
	Multiplicity mult_,
	boolean isProduct_,
	boolean isAbstract_) {
        super(location_, name_, extends_, subsets_, decls_, fact_);
        Dbg.chk(extends_.numChildren() <= 1);
        _mult = (mult_.equals(Multiplicity.NONE) ? Multiplicity.SET : mult_);
        _isProduct = isProduct_;
        _isAbstract = isAbstract_;
    }


    /** constructor for creating dummy signature */
    public Signature(QualifiedName name_) {
        this(
            Location.UNKNOWN,
            name_,
            new SigExprs(),
            new SigExprs(),
            new Decls(),
            new Fact(new QualifiedName(Id.generateId("Fact"), name_.getPath())),
	    Multiplicity.SET,
            false,
            false);
    }

    //GET AND SET METHODS

    /**
     * gets the name of this
     * @return the {@link QualifiedName}
     */
    public QualifiedName getName() {
        return (QualifiedName)childAt(NAME_INDEX);
    }

    /** set the Name of this */
    public void setName(QualifiedName newChild_) {
        setChild(NAME_INDEX, newChild_);
    }

    /**
     * Gets a string representing the name of this with the parameters
     * passed to instantiate it.  This must be typed before this method
     * is called.  Also, this only works properly when the signature is
     * not instantiated with subsignatures.
     */
    public String getTypedName() {
        Dbg.chk(_unionType != null, "attempt to get typed name before typing");
        StringBuffer ret = new StringBuffer(getName().nodeString());
        return ret.toString();
    }

    /**
     * gets the extended signature names of this
     * @return the {@link SigExprs}
     */
    public SigExprs getExtends() {
        return (SigExprs)childAt(EXTENDS_INDEX);
    }

    /** set the Extends of this */
    public void setExtends(SigExprs newChild_) {
        setChild(EXTENDS_INDEX, newChild_);
    }

     /**
     * gets the superset signature names of this
     * @return the {@link SigExprs}
     */
    public SigExprs getSubsets() {
        return (SigExprs)childAt(SUBSETS_INDEX);
    }

    /** set the Subsets of this */
    public void setSubsets(SigExprs newChild_) {
        setChild(SUBSETS_INDEX, newChild_);
    }


    /**
     * gets the decls of this
     * @return the {@link Decls}
     */
    public Decls getDecls() {
        return (Decls)childAt(DECLS_INDEX);
    }

    /** set the Decls of this */
    public void setDecls(Decls newChild_) {
        setChild(DECLS_INDEX, newChild_);
    }

    /**
     * gets the fact of this
     * @return the {@link Fact}
     */
    public Fact getFact() {
        return (Fact)childAt(FACT_INDEX);
    }

    /** set the Fact of this */
    public void setFact(Fact newChild_) {
        setChild(FACT_INDEX, newChild_);
    }

    /**
     * gets the multiplicity of this
     * @return the {@link Fact}
     */
    public Multiplicity getMult() {
        return _mult;
    }

    /** sets the multiplicity of this */
    public void setMult(Multiplicity newMult_) {
        _mult = newMult_;
    }

    /**
     * Returns the isAbstract.
     * @return boolean
     */
    public boolean isAbstract() {
        return _isAbstract;
    }

    /**
     * Sets the isAbstract.
     * @param isAbstract The isAbstract to set
     */
    public void setAbstract(boolean isAbstract_) {
        _isAbstract = isAbstract_;
    }

    /**
     * get the product setting for this
     * @return true if this is product, false otherwise
     */
    public boolean isProduct() {
        return _isProduct;
    }

    /**
     * set the product setting for this
     * @param isProduct_ the new product setting
     */
    public void setProduct(boolean isProduct_) {
        _isProduct = isProduct_;
    }


    public LeafId getLeafId() {
        return _id;
    }

    public void setLeafId(LeafId id_) {
        _id = id_;
    }

    /**
     * @return true if this signature was declared to be "in" another signature,
     * otherwise returns false
     **/
    public boolean isSubset() {
        return getSubsets().getSigExprIter().hasNext();
    }


    /**
     * get the local scope of this
     * @return the LocalScope
     */
    public LocalScope getLocalScope() {
        return _localScope;
    }

    /**
     * set the local scope of this
     * @param localScope_ the new LocalScope
     */
    public void setLocalScope(LocalScope localScope_) {
        _localScope = localScope_;
    }

    /**
     * add a pointer to a Signature which extends this
     * @param sig_ the extending Signature
     */
    public void addExtBy(Signature sig_) {
        _extendedBy.add(sig_);
    }

    /**
     * get an iteration of the Signatures which extend this
     * @return the Iterator
     */
    public Iterator getExtByIter() {
        return _extendedBy.iterator();
    }

    /**
     * @param sig_ a Signature
     * @return true if this is extended by sig_
     */
    public boolean isExtBy(Signature sig_) {
        return _extendedBy.contains(sig_);
    }


    /** 
     * Gets the UnionType of this.  If this is not declared with
     * the "in" notation, than the returned UnionType is simply
     * the degenerate union with only one term -- the SigType
     * of this wrapped in a Relation.
     * @return the UnionType of this
     **/
    public UnionType getUnionType() {
        return _unionType;
    }

    /**
     * Sets the UnionType of this.  The operation is valid only
     * on signature that are subsets.  Calling the procedure on
     * a non-subset signature will cause a fatal error.
     * @param unionType_ the new UnionType_
     **/
    public void setUnionType(UnionType unionType_) {
        Dbg.chk(isSubset(), "attempted to set a UnionType for a non-subset");
        _unionType = unionType_;
    }
    /**
     * Gets the SigType of this, if this is not declared with
     * the "in" notation.   
     * @return the SigType of this or null (if this is a subset)
     */
    public SigType getSigType() {
        return _sigType;
    }

    /**
     * Sets the SigType of this. The operation is valid only
     * on signature that are NOT subsets.  Calling the procedure on
     * a subset signature will cause a fatal error. 
     * @param sigType_ the new SigType
     */
    public void setSigType(SigType sigType_) {
        Dbg.chk(!isSubset(), "attempted to set a SigType for a subset");
        _sigType = sigType_;
        _unionType = new UnionType(new RelationType(sigType_));
    }

    /**
     * returns a SigExpr 
     * @return SigExpr representing this Signature
     */

    public SigExpr toSigExpr() {
        QualifiedName sigExprName = getName();
        SigExpr ret = new SigExpr(Location.UNKNOWN, sigExprName);
        ret.setType(getUnionType());
        if (_id != null) {
            ret.setLeafId(_id);
        }
        return ret;
    }

    /**
     * accept an AST visitor
     * @param visitor_ the visitor
     */
    protected void acceptVisitor(ASTVisitor visitor_) {
        visitor_.visit(this);
    }

    /**
     * accept a returning AST visitor
     * @param visitor_ the visitor
     * @return the Object returned by the visitor
     */
    protected Object acceptReturnVisitor(ASTReturnVisitor visitor_) {
        return visitor_.visit(this);
    }

    /**
     * Checks if an object is equal to this.  We define equality
     * for signatures as having equal qualified names.
     * @param obj the object to compare
     * @return <pre>true</pre> if obj is equal to this; <pre>false</pre> otherwise
     */
    public boolean equals(Object obj) {
        return ((obj instanceof Signature) && (getName().equals(((Signature)obj).getName())));
    }

    public int hashCode() {
        return getName().hashCode();
    }

    public String nodeString() {
        StringBuffer ret =
            new StringBuffer(
                "sig "
		+ getName().getId().nodeString()
		+ getExtends().childrenStr(" extends ", ", ", "")
		+ getSubsets().childrenStr(" in " ,", ", "")
		+ " { "
		+ getDecls().childrenStr("", ", ", "")
		+ " } ");
        if (!((getFact().isEmpty()))) {
            ret.append(" " + getFact().getFormula().nodeString());
        }
        return ret.toString();
    }

    /**
     * performs typical copy, and then clears the <pre>extendedby</pre> pointers,
     * the local scope, and the sig type of the copy
     * @return a copy of this
     */
    public Object copy() {
        Signature sigCopy = (Signature)super.copy();
        sigCopy._sigType = null;
        sigCopy._extendedBy = new LinkedHashSet();
        sigCopy._localScope = new LocalScope();
        return sigCopy;
    }

    /**
     * lookup the type of a field of this.  this lookup mechanism
     * assumes that the lookup for a field will always start at
     * a signature which does not extend any other signatures, ie.
     * when looking up a field of a signature, get its type, get
     * the signature that the type points to, and look the field up
     * from there.
     * @param field_ the field to lookup
     * @return the type of the field, or null if the field is not found
     */
    public UnionType getFieldType(String field_) {
        UnionType retType = null;

        // lookup the field in the local scope of this
        retType = _localScope.lookupType(field_);

        if (retType == null) {
            // try to find the field in the signatures which
            // extend this
            Iterator extSigIter = _extendedBy.iterator();
            while (extSigIter.hasNext()) {
                retType = ((Signature)extSigIter.next()).getFieldType(field_);
                if (retType != null)
                    break;
            }
        }

        return retType;
    }

    public void setLeafIdMap(LeafIdMap leafIdMap_) {
        _leafIdMap = leafIdMap_;
    }

    public LeafIdMap getLeafIdMap() {
        return _leafIdMap;
    }

    public LeafId getFieldLeafId(String field_) {
        LeafId fieldId = null;
        // lookup in local mapping
        fieldId = _leafIdMap.lookupLeafId(field_);
        if (fieldId == null) { // not in local mapping
            // lookup in extending sigs
            Iterator extSigIter = _extendedBy.iterator();
            while (extSigIter.hasNext()) {
                fieldId = ((Signature)extSigIter.next()).getFieldLeafId(field_);
                if (fieldId != null)
                    break;
            }
        }
        return fieldId;
    }

    /*
     * the field info methods above don't do quite what the solution instance code 
     * needs.  from the perspective of an atom in the instance, you want to look
     * up the fields in an upwards manner, i.e. check supertypes too, but in terms
     * of type checking, etc., you want to be able to downcast and check subsigs too     
     * 
     */

    /**     
     * @return all field names (String's) of this signature and any 
     * super-signatures 
     */
    public Set getAllFieldNames() {
        if (_allFieldNames == null) {

            _allFieldNames = new HashSet();
            
            // can't use leafIdMap to get this info because (1) if B is a sub*set* of A
            // and has a field, that field will show up in A's leafidmap, and (2) 
            // atomization leaves behind trails in that map.  Instead, look straight  
            // at the parsed ast info             
            for (Iterator declIter = getDecls().getDeclIter(); declIter.hasNext(); ) {
            	Decl decl = (Decl)declIter.next();
            	for (Iterator varIter = decl.getVariables().getVariableIter(); varIter.hasNext(); ) {
            		Variable var = (Variable)varIter.next();
            		_allFieldNames.add(var.getId().nodeString());
            	}
            }
            
            
            // lookup in super type

            if (_sigType.getSuperType() != null) {
                _allFieldNames.addAll(_sigType.getSuperType().getSignature().getAllFieldNames());
            }
        }

        return _allFieldNames;
    }

    public LeafId searchFieldLeafIdUpwards(String field_) {
        LeafId fieldId = null;

        // lookup in local mapping
        fieldId = _leafIdMap.lookupLeafId(field_);
        if (fieldId == null) { // not in local mapping
            if (_sigType.getSuperType() != null) {
                fieldId = _sigType.getSuperType().getSignature().searchFieldLeafIdUpwards(field_);
            }
        }
        return fieldId;
    }

    public UnionType searchFieldTypeUpwards(String field_) {
        UnionType retType = null;

        // lookup the field in the local scope of this
        retType = _localScope.lookupType(field_);

        if (retType == null) {
            // look in supertype
            if (_sigType.getSuperType() != null) {
                retType = _sigType.getSuperType().getSignature().searchFieldTypeUpwards(field_);
            }
        }

        return retType;
    }


    public String toString() {
        return "Signature: " + getName().toString();
    }

    /**
     * Assumes that expr_ is an AST representing a sum of SigExprs. Adds the extracted
     * SigExprs to this._subsetOf
     * @param expr_ Expr from which SigExprs will be extracted
     **/
    //    private void _extractSigExprsFromExpr(Expr expr_) {
    //
    //	if (expr_ instanceof BinaryExpr) {
    //	    BinaryExpr sum = (BinaryExpr) expr_;
    //	    Dbg.chk(sum.getOp().getOpCode() == BinaryExprOp.UNION, 
    //		    "attempted to subset an expression that is not a sum of SigExpr");
    //	    _extractSigExprsFromExpr(sum.getLeft());
    //	    _extractSigExprsFromExpr(sum.getRight());
    //	} else if (expr_ instanceof SigExpr) {
    //	    _subsetOf.add(expr_);
    //	} else {
    //	    Dbg.fatal("attempted to subset an expression that is not a sum of SigExpr");
    //	}
    //    }

}
